Step of Proof: filter_fseg 11,40
Inference at * 
Iof proof for Lemma filter fseg:


  T:Type, P:(T), L2, L1:(T List). fseg(T;L1;L2)  fseg(T;filter(P;L1);filter(P;L2)) 
latex
 by ((((((Auto) 
CollapseTHEN (ParallelOp ( -1)))) 
CollapseTHEN (ExRepD))) 
CollapseTHEN (
C((((((if (first_bool T:b) then HypSubst' else RevHypSubst') ( -1)( 0))) 
CollapseTHENA (Auto))
C) 
CollapseTHEN (((((InstConcl [filter(P;L)]) 
CollapseTHEN (Auto))) 
CollapseTHEN (((
CRWO "filter_append" 0) 
CollapseTHEN (Auto)))))))) 
latex

C.

Definitionsfilter(P;l), fseg(T;L1;L2), ||as||, i  j , A  B, P  Q, P  Q, P & Q, [car / cdr], , SQType(T), P  Q, {T}, , {x:A| B(x)} , t  T, , x:A. B(x), x:A  B(x), Type, s = t, type List, as @ bs, x:A. B(x), x:AB(x), s ~ t
Lemmasbool wf, fseg wf, non neg length, cons one one, guard wf, nat wf, member wf, filter append

origin